| Definitions | x:A  B(x), s = t, Knd, d-decl(D;i), d-world-state(D;i),  x:A. B(x), left + right, P  Q, P & Q, x:A  B(x), Dsys, Feasible(D), Atom$n, Id, {x:A| B(x)} ,  ,  x:A. B(x), Unit, Type, IdLnk, Void, ma-prob(M;b), Outcome, b  dom(M.prob), M.state,  , P   Q, False,  A, A  B,  , #$n, n - m, d-comp(D; v; sched; dec; d), CV(F), f(a), t.1, M(i), M.init(x)?v,  x.A(x), (i = j), if b then t else f fi , M.(timed)state, t T, {i..j },  b,  ,  b, P  Q, timedState(ds), -n, n+m, a < b, S  T, i j < k, suptype(S; T), hd(l), let x = a in b(x), d-partial-world(D;f;t';s;d), World, True, i z j, p q, queue(l;t), Msg, ||as||, i <z j, destination(l), i = j, p  q,  T, P Q, doact(k;v), i  j , mtag(m), rcv(l,tg), Msg(M), w.M, mval(m), M.dout(l,tg), {T}, tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), locl(a), w-action-dec(TA;M;i), a = b, mlnk(m), source(l), <a, b>, MsgA, shift-state(s), stutter-state(s), next-world-state(D;i;s;k;v), M.da(a),  , M.ds(x), read-state(s), M.ef(k,x,s,v)?w, M.din(l,tg), M.Msg, type List, M.sends(k,s,v), null, w-knum(w;i;k;t), finite-type(T), Feasible(M), ma-prob-da(M), inr x , s ~ t, case b of inl(x) => s(x) | inr(y) => t(y), f(x)?z |
| Lemmas | w-knum wf, locl wf, ma-da wf, subtype rel list, filter type, ma-msg wf, mlnk wf d, ma-send-val wf, doact wf, d-decl-subtype, shift-state wf, ma-ef-val wf, read-state wf, mval wf, d-decl wf, next-world-state wf, stutter-state wf, ma-dout wf, msga wf, lsrc wf, mlnk-hd-w-queue, assert-d-eq-Loc, assert-eq-id, eq id wf, not rcv locl, rcv one one, Knd wf, rcv wf, hd wf, assert of band, and functionality wrt iff, assert of lt int, squash wf, true wf, bnot thru band, bnot of lt int, assert of bor, or functionality wrt iff, assert of le int, band wf, d-eq-Loc wf, ldst wf, lt int wf, length wf1, w-Msg wf, w-queue wf, bor wf, le int wf, subtype rel self, world wf, d-partial-world wf, CV wf, le wf, ma-init-val wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bnot wf, not wf, assert wf, d-comp wf2, int seg wf, d-world-state wf, d-feasible wf, bool wf, ma-st wf, ifthenelse wf, ma-prob-dom wf, p-outcome wf, ma-prob wf, ma-tst wf, d-m wf, Id wf, nat wf, IdLnk wf, unit wf, dsys wf, nat properties |
dec:(i,a:Id